es:event_system{i:l}, e,a:es-E(es).
es-locl(es; a; e)
 (b:es-E(es). (((es-first(es; b))) c ((a = es-pred(es; b))  es-le(es; b; e)))) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), A c B, P  Q, t  T, prop{i:l}, x. t(x), wellfounded{i:l}(A; x,y.R(x;y)), x(s), guard(T), P  Q, P  Q
Lemmas	es-locl-wellfnd, es-E wf, es-locl wf, not wf, assert wf, es-first wf, es-pred wf, es-le wf, es-locl-iff, event system wf, es-le-self, es-pred-locl, es-locl transitivity1, es-le weakening